es:ES, X:AbsInterface(Top), z:(E List). es-interface-sublist(X;z)  (E(X) List) 

latex

Definitions

t  T, s = t, x:AB(x), x:A. B(x), Top, e  X, b, Type, , ES, AbsInterface(A), type List, E, x.A(x), filter(P;l), E(X), {x:A| B(x)} , a:A fp B(a), strong-subtype(A;B), P  Q, x:A  B(x), left + right, let x,y = A in B(x;y), t.1, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , , A List, [car / cdr], A, ff, b, P & Q, P  Q, p =b q, i <z j, i z j, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), e = e', p  q, p  q, p q, tt, , Unit, [], es-interface-sublist(X;z)

Lemmas

event system wf, es-interface wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, bool wf, member wf, es-E-interface wf, es-E wf, subtype rel wf, assert wf, top wf, es-is-interface wf